# [isabelle] pushing let environments to the top level

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.*