*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Common sub-expression elimination*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 19 Jan 2016 12:18:12 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CAMej=24d6OGW9gr_D6Z98To1x=_=G9UM=+9tDcFv3ee0ak5cSw@mail.gmail.com>*References*: <569E105D.1000807@in.tum.de> <CAMej=24d6OGW9gr_D6Z98To1x=_=G9UM=+9tDcFv3ee0ak5cSw@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.1

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

**Follow-Ups**:**Re: [isabelle] Common sub-expression elimination***From:*Andreas Lochbihler

**References**:**[isabelle] Common sub-expression elimination***From:*Manuel Eberl

**Re: [isabelle] Common sub-expression elimination***From:*Ramana Kumar

- Previous by Date: Re: [isabelle] Dockable panels
- Next by Date: Re: [isabelle] Dockable panels
- Previous by Thread: Re: [isabelle] Common sub-expression elimination
- Next by Thread: Re: [isabelle] Common sub-expression elimination
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list