*To*: Manuel Eberl <eberlm at in.tum.de>, Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] Common sub-expression elimination*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 25 Jan 2016 09:38:47 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <569E1B74.8000507@in.tum.de>*References*: <569E105D.1000807@in.tum.de> <CAMej=24d6OGW9gr_D6Z98To1x=_=G9UM=+9tDcFv3ee0ak5cSw@mail.gmail.com> <569E1B74.8000507@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

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

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

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

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

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

- Previous by Date: [isabelle] "defines" in a locale
- Next by Date: Re: [isabelle] "defines" in a locale
- Previous by Thread: Re: [isabelle] Common sub-expression elimination
- Next by Thread: [isabelle] Postdoc position on security protocol verification at NTU Singapore
- 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