# Re: [isabelle] How tactic fold instantiates variables

*To*: Daniel Raggi <danielraggi at gmail.com>
*Subject*: Re: [isabelle] How tactic fold instantiates variables
*From*: Makarius <makarius at sketis.net>
*Date*: Tue, 23 Jun 2015 23:17:14 +0200 (CEST)
*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*In-reply-to*: <CAFzz2xQ413v8dp1jWbN2B0=qi-kJNT+kR3yfVW=ZKtG-UwMQnA@mail.gmail.com>
*References*: <CAFzz2xQ413v8dp1jWbN2B0=qi-kJNT+kR3yfVW=ZKtG-UwMQnA@mail.gmail.com>
*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

(This old thread still looks unsettled.)
On Fri, 29 May 2015, Daniel Raggi wrote:

When folding a definition, why would someone (in some cases), need to
specify instantiations of variables using [where "X = ..."]?
I can see how it's useful to do it in some cases to avoid having to
backtrack.

First note that (fold eq) is the same as (unfold eq [symmetric]).

`For more than one equation, there is a slight difference in the initial
``order, although the details are unclear to me; see
``src/Pure/raw_simplifer.ML:
`
val rev_defs = sort_lhs_depths o map Thm.symmetric;

`Larry might be able to explain that code "from the depths of time", as he
``usually says; see
`http://isabelle.in.tum.de/repos/isabelle/rev/e7588b53d6b0

`Back to "unfold". That is just the Simplifier with its usual policies,
``see also the isar-ref manual section 9.3 "The Simplifier". The main
``strategy is bottom-up rewriting with higher-order patterns.
`

`There is no support for back-tracking in the rewrite engine, so the
``command 'back' normally does not make any sense with applications of
``"unfold", "simp" etc. (In principle some wrapper tactics of the
``simplifier can produce more than one result for back-tracking.)
`

I've defined function *fadd* as follows:
*definition "fadd M N = (Îa. M a + N a)"*
purely as a test, I have the following goal to prove:
*lemma "(Îx. 0 + 0) = (Îx. 0)"*
However, when I try this:
*lemma "(Îx. 0 + 0) = (Îx. 0)"*
* apply (fold fadd_def)*
I get *(Îx. fadd (Îa. 0) (Îa. a) 0) = (Îx. 0) *as a result. However, if I
try:
lemma "(Îx. 0 + 0) = (Îx. 0)"
* apply (fold fadd_def[where M = "Îx. 0" and N = "Îx. 0"]) *
I get what I want, which is *fadd (Îx. 0) (Îx. 0) = (Îx. 0)*.
I'm a bit confused, because in the case of *apply (fold fadd_def) *I'm not
even getting what I want, even when using *back*. Can anyone point me at
why my desired instantiation of variables is not tried?

`Looking quickly over the example, it looks as an expected result of
``bottom-up rewriting.
`

`What you want, might be something else. Depending on the application, you
``can try a simproc to determine instantiations in ML, or you can try to
``implement your very own replacement strategy as a conversion in ML.
`

`The latter is actually easier than writing common tactics, although less
``known. The starting point is src/Pure/conv.ML and examples may be found
``in existing Isabelle sources, although that structure Conv is exceptional
``in being used as "open" in Isabelle/ML, i.e. it requires a hypersearch
``with unqualified names.
`
Makarius

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