求助：如何为Isabelle的MPair构造定义多元素支持的语法

核心思路 #

由于MPair是二元构造函数，要支持3个及以上元素的元组语法，需通过递归嵌套扩展翻译规则，让多元素的⦃x₁, x₂, ..., xₙ⦄自动展开为嵌套的MPair结构。

完整实现代码 #

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

syntax
  "_mpair" :: "args ⇒ msg"    ("⦃(_)⦄")
translations
  "⦃x, y⦄" == "msg.MPair x y"
  "⦃x, y, z, xs⦄" == "⦃x, ⦃y, z, xs⦄⦄"

规则说明 #

• 基础规则：⦃x, y⦄直接映射为二元MPair x y，覆盖2元素场景。
• 递归规则：当元素数量≥3时，将第一个元素与剩余元素组成的子元组嵌套，自动展开为多层MPair。示例：
  • ⦃a,b,c⦄翻译为MPair a (MPair b c)
  • ⦃a,b,c,d⦄翻译为MPair a (MPair b (MPair c d))

验证示例 #

在Isabelle中输入以下代码测试：

term "⦃Agent Server, Nonce 1, Key 2⦄"

输出结果为：msg.MPair (msg.Agent Server) (msg.MPair (msg.Nonce 1) (msg.Key 2))，符合预期。

可选调整：左结合嵌套 #

若需要左结合结构（如MPair (MPair a b) c），修改递归翻译规则为：

translations
  "⦃x, y⦄" == "msg.MPair x y"
  "⦃x, y, z, xs⦄" == "⦃⦃x, y⦄, z, xs⦄"

内容的提问来源于stack exchange，提问作者Kookie