# Re: [isabelle] syntax

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*