*To*: Ewaryst Schulz <ewaryst.schulz at dfki.de>*Subject*: Re: [isabelle] pushing let environments to the top level*From*: Konrad Slind <slind at cs.utah.edu>*Date*: Sat, 25 Apr 2009 17:43:28 -0600*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <49F18DB9.3000802@dfki.de>*References*: <49F18DB9.3000802@dfki.de>

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 liketo push them to the top of the formula and ideally declare them bydef-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, ands1(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 existingprocedure to do that automatically. Is there a tactic which doesexactly this job?Of course then I won't have the defs visible in my isar proof, andI'd need a labeling convention for this knowledge (to access theequalities yi == t1(...)).The method should also fail if the Y,yk and X intersect in thevariable 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 environmentsdeep 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 -------------------------------------------------------------

**Follow-Ups**:**Re: [isabelle] pushing let environments to the top level***From:*Brian Huffman

**References**:**[isabelle] pushing let environments to the top level***From:*Ewaryst Schulz

- Previous by Date: [isabelle] Call for Papers: Formal Aspects of Component Software (FACS 2009)
- Next by Date: [isabelle] CFP: TPHOLs 2009 --EMERGING TRENDS--
- Previous by Thread: [isabelle] pushing let environments to the top level
- Next by Thread: Re: [isabelle] pushing let environments to the top level
- Cl-isabelle-users April 2009 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