Re: [isabelle] pushing let environments to the top level



Hi,

  Michael Norrish and I tackled exactly this sort of thing in

   http://www.cs.utah.edu/~slind/papers/tphols05.pearl.pdf

The ideas in the paper are worked out in HOL4, and may
need to be modified a bit for Isabelle/HOL.

Cheers,
Konrad.

On Apr 24, 2009, at 4:00 AM, Ewaryst Schulz wrote:

Hi,
I have a question regarding let environments in formulas. I'd like to push them to the top of the formula and ideally declare them by def-statements in the isar-proof.
Consider e.g. a context with variables x1, ..., xn:
My goal is of the form Psi(s1(X), ... , sm(X)), where X = x1, ..., xn, and
s1(X) of the form

let y1 = t1(X);
    y2 = t2(X,y1);
    ...
    yk = tk(X,Y)
in Phi(X,Y,yk)

Now I'd like to move the let-environment to the outside (theoretically this is possible, if no variable capturing occurs, by some beta/eta reduction and expansion):

Psi(s1(X), ... , sm(X))
--->
let y1 = t1(X);
    y2 = t2(X,y1);
    ...
    yk = tk(X,Y)
in Psi(Phi(X,Y,yk), s2(X), ... , sm(X))

And then put the let-env to the isar context by def:

--->
def y1 == t1(X)
def y2 == t2(X,y1)
...
def yk == tk(X,Y)

goal:
Psi(Phi(X,Y,yk), s2(X), ... , sm(X))

I'm not a really advanced user so I'd prefer to use an existing procedure to do that automatically. Is there a tactic which does exactly this job? Of course then I won't have the defs visible in my isar proof, and I'd need a labeling convention for this knowledge (to access the equalities yi == t1(...)). The method should also fail if the Y,yk and X intersect in the variable names (variable capturing). I don't think there is already something which does that exactly, but perhaps there is a better way to deal with let environments deep inside formulas
(I don't want to expand/unfold the let environment!) ?

Thanks for your help in advance,

cheers,
Ewaryst



--
- ------------------------------------------------------------------
Ewaryst Schulz                        office @ Universität Bremen:
Junior Researcher                     Cartesium 2.049
Safe and Secure Cognitive Systems     Enrique-Schmidt-Str. 5
DFKI-Lab Bremen                       FB3 Mathematik - Informatik
Robert-Hooke-Str. 5                   Universität Bremen
D-28359 Bremen                        P.O. Box 330 440
                                     D-28334 Bremen
phone: (+49) 421-218-64274            Fax:   (+49) 421-218-9864216
mail: Ewaryst.Schulz at dfki,de
www.dfki.de/sks/staff/ewschulz
------------------------------------------------------------------


-------------------------------------------------------------
Deutsches Forschungszentrum für Künstliche Intelligenz GmbH
Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern

Geschäftsführung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313
-------------------------------------------------------------






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