*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] syntax*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Wed, 21 Dec 2011 13:59:03 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAAMXsiauwLhCW6rwZ3-msFSo+ddmZmZ1dt=1AM+6W8uSrBkmDA@mail.gmail.com>*References*: <4EF058F9.3040700@abo.fi> <CAAMXsiauwLhCW6rwZ3-msFSo+ddmZmZ1dt=1AM+6W8uSrBkmDA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:8.0) Gecko/20111124 Thunderbird/8.0

Hello Brian, Thank you very much. It works nicely. It seems that the syntax [: x, y := x', y' . ... :] works together with the syntax [: R :] = update R when R has the type 'a => ('a set). Viorel On 12/20/2011 12:04 PM, Brian Huffman wrote:

On Tue, Dec 20, 2011 at 10:44 AM, Viorel Preoteasa <viorel.preoteasa at abo.fi> wrote:Hello, I have a programming construct construct of the following form: update (% (x::'a, y::'b, z::'c): {(x'::', y'::'b, z::'c) . x' = x+1 /\ y'=y / 2 /\ z' = z + x + y}) Is it possible to introduce the syntax: [: x::'a, y::'b, z::'c := x'::'a, y'::'b, z::'c . x' = x+1 /\ y'=y / 2 /\ z' = z + x + y :]Here's something that's close to what you want. It does require parentheses around the tuples of variable bindings, though. (The nonterminal "pttrn" is what is used for the binders in lambda abstractions and set comprehensions.) syntax "_foo" :: "pttrn => pttrn => logic => logic" ("[: _ := _ . _:]") translations "_foo x y t" == "CONST update (_abs x (_Coll y t))" term "[: (x::'a, y::'b) := (x'::'a, y'::'b) . P x y x' y' :]" And here's another variant where the parentheses are not required. It's a little more awkward to define because the syntax translation needs to convert from nonterminal "patterns" (defined in HOL/Product_Type.thy, used for tuple binders) to nonterminal "pttrn". syntax "_foo" :: "patterns => patterns => logic => logic" ("[: _ := _ . _:]") translations "_foo (_patterns x xs) (_patterns y ys) t" == "CONST update (_abs (_pattern x xs) (_Coll (_pattern y ys) t))" "_foo x y t" == "CONST update (_abs x (_Coll y t))" term "[: x::'a, y::'b := x'::'a, y'::'b . P x y x' y' :]" - Brian

**References**:**[isabelle] syntax***From:*Viorel Preoteasa

**Re: [isabelle] syntax***From:*Brian Huffman

- Previous by Date: [isabelle] Using schematic_lemma to avoid boilerplate
- Next by Date: Re: [isabelle] Using schematic_lemma to avoid boilerplate
- Previous by Thread: Re: [isabelle] syntax
- Next by Thread: [isabelle] Using schematic_lemma to avoid boilerplate
- Cl-isabelle-users December 2011 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