So I'm trying to define syntax for the abbreviation provided in section 10.2 near the end of page 189 of https://isabelle.in.tum.de/doc/tutorial.pdf, but I'm not sure how. I tried looking at the list syntax definition from https://isabelle.in.tum.de/library/HOL/HOL/List.html, but I noticed that the MPair datatype constructor shown below takes a minimum of 2 arguments, not 0.
datatype agent = Server | Friend nat | Spy
type_synonym key = nat
consts invKey :: "key ⇒ key" (*matches public key to private key, and vice versa.*)
datatype msg = Agent agent
| Nonce nat
| Key key
| MPair msg msg
| Crypt key msg
I tried defining the syntax as follows:
syntax
"_list" :: "args => msg" ("⦃(_)⦄")
translations
"⦃x, y⦄" == "msg.MPair x y"
The syntax definition works for two elements, but not 3 or more. Can I please have some help?
Thanks in advance!
If you compare the syntax translation rule for lists with yours, you should notice that yours are not recursive anymore. Therefore, it makes sense that they are only defined for precisely two elements.
Adding recursion as in the case of Lists would look like this:
syntax
"_msgSet" :: "args => msg" ("⦃(_)⦄")
translations
"⦃x, y, z⦄" == "msg.MPair x ⦃y, z⦄"
"⦃x, y⦄" == "msg.MPair x y"
This has the effect that the following are valid terms:
term "⦃y, z⦄"
term "⦃x, y, z⦄"
term "⦃x, y, z, Nonce 23⦄"
I assumed your MPair constructor to associate from the right. For lists the associativity is given by the asymmetry of types. This is not the case with MPair—so I had to make a guess.
You might notice that the base case of my recursive definition has two elements and not just one, if we compare to the base case of lists:
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
The reason for this is that your datatype does not provide a wrapper for singletons but only pairs. So I did not know what semantics to assign to:
term "⦃z⦄" (*undefined ?*)