# Re: [isabelle] Common sub-expression elimination

```The let_simp simproc in HOL.thy already does some sort of CSE in special cases. Try, e.g.,

lemma "P (let x = f y in x + x + f y)"
apply simp

```
CSE can be great for specific applications (like approximation), but the current state with let is a mess. If you have a clear idea how to control CSE (and deal with let), I'd be all in favour of cleaning up let_simp.
```
Best,
Andreas

On 19/01/16 12:18, Manuel Eberl wrote:
```
```Yes, you can, of course, always do that, and maybe this is also the best way to do it.

I was thinking of having a "Let"-like construct on the expression level and then using
that to eliminate the subexpressions. Or with approximate, the way you would eliminate a
common sub-expression would be to rewrite something like "pi + pi â {0..10}" to "âx. x =
pi â x + x â {0..10}", which causes approximate to approximate pi, store the bounds it
finds in some context under the name "x", and re-uses these bounds whenever it encounters
"x" from then on.

However, I suppose you could also achieve this by first rewriting it to "let x = pi in x +
x â {0..10}" with the CSE tool and then rewriting that to "âx. x = pi â x + x â {0..10}"
outside the CSE tool.

This might be a nicer solution.

Manuel

On 19/01/16 11:48, Ramana Kumar wrote:
```
```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
<mailto: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.