*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Dealing with lets in Isar*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Fri, 29 Nov 2013 20:40:02 +0000*Accept-language*: en-US, en-AU*Cc*: "christian.urban at kcl.ac.uk" <christian.urban at kcl.ac.uk>, "xingyuanzhang at 126.com" <xingyuanzhang at 126.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5298C0F1.80605@inf.ethz.ch>*References*: <k28mb9$1ir$1@ger.gmane.org> <5047E49D.9070307@in.tum.de> <k2a3j4$qdh$1@ger.gmane.org> <m2mwkn5hk1.fsf@kcl.ac.uk>,<5298C0F1.80605@inf.ethz.ch>*Thread-index*: AQHO7RwUeoaVTtcATUCOk25is0+30Jo7rcSAgAD+X1I=*Thread-topic*: [isabelle] Dealing with lets in Isar

You can implement a nice expansion of lets into equations with the simplifier as per Konrad Slimd's and my proof pearl paper in TPHOLs 2005 Michael > On 30 Nov 2013, at 3:35, "Andreas Lochbihler" <andreas.lochbihler at inf.ethz.ch> wrote: > > Hi Christian, > > I don't completely understand why this is related to let. A let just introduces an abbreviation. However, in your example, you are more concerned with patterns such as tuples, but > > let (x, y) = e in f x y > > is syntactic sugar for > > Let e (prod_case (%x y. f x y)) > > So, do you also want to introduce variables if there's no pattern-matching involved, such that "P (let x = e in f x)" gets transformed into "!!x. x = e ==> P (f x)"? > > In principle, you can use Isabelle's splitter: > > lemma Let_prod_split_asm: > "P (Let e (prod_case f)) = (~ (EX x y. (x, y) = e & ~ P (f x y)))" > by(auto simp add: Let_def prod.split_asm) > > lemma Let_split_asm: "P (Let e f) = (~ (EX x. x = e & ~ P (f x)))" > by(auto simp add: Let_def) > > lemma > assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)" > shows "thesis" > using assms > apply - > proof(split Let_prod_split_asm Let_split_asm)+ > case (goal1 x y u v w k) > > With some ML programming, it should be easy to make this more readable. > > Hope this helps, > Andreas > > >> On 29/11/13 16:55, Christian Urban wrote: >> >> Dear All, >> >> We have a question about how to deal conveniently with >> Lets in Isar proofs. Some of our definitions contain many >> nested lets, as in >> >> definition >> "foo f e1 e2 e3 == let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k" >> >> >> The problem is that we have foo unfolded in our premises, say >> >> lemma >> assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)" >> shows "thesis" >> >> We could prove such lemmas with >> >> lemma >> assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)" >> shows "thesis" >> proof - >> from assms >> obtain x y u v w k >> where "P (f x y u v w k)" and >> "(x, y) = e1" and "(u, v) = e2" and "(w, k) = e3" by ... >> >> but we are wondering whether there is a simpler way. Essentially, >> we want to avoid having to fix the variables and to avoid to write >> the equations explicitly. We rather prefer the way how the cases-construction >> works, which automatically fixes variables and puts such equations >> into the context, for example >> >> lemma >> assumes "P (n:: nat)" >> shows "thesis" >> proof (cases n) >> >> In this example you have "n = 0" in the "first" case and fix nat/n = Suc nat >> in the "second" case. Is there something similar for many nested lets? >> >> If not, how would we have to go about implementing (presumably in ML) >> such a construction? >> >> Best wishes, >> Christian > ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

**References**:**[isabelle] Dealing with lets in Isar***From:*Christian Urban

**Re: [isabelle] Dealing with lets in Isar***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Accessing slightly old versions of Isabelle
- Next by Date: [isabelle] Knaster-Tarski Lemma
- Previous by Thread: Re: [isabelle] Accessing slightly old versions of Isabelle
- Next by Thread: [isabelle] Knaster-Tarski Lemma
- Cl-isabelle-users November 2013 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