*To*: <christian.urban at kcl.ac.uk>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Dealing with lets in Isar*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 29 Nov 2013 17:29:37 +0100*Cc*: xingyuanzhang at 126.com*In-reply-to*: <m2mwkn5hk1.fsf@kcl.ac.uk>*References*: <k28mb9$1ir$1@ger.gmane.org> <5047E49D.9070307@in.tum.de> <k2a3j4$qdh$1@ger.gmane.org> <m2mwkn5hk1.fsf@kcl.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.1

Hi Christian,

let (x, y) = e in f x y is syntactic sugar for Let e (prod_case (%x y. f x y))

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

**Follow-Ups**:**[isabelle] Accessing slightly old versions of Isabelle***From:*Andrew Butterfield

**Re: [isabelle] Dealing with lets in Isar***From:*Michael Norrish

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

- Previous by Date: [isabelle] Dealing with lets in Isar
- Next by Date: [isabelle] Accessing slightly old versions of Isabelle
- Previous by Thread: [isabelle] Dealing with lets in Isar
- Next by Thread: [isabelle] Accessing slightly old versions of Isabelle
- 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