CODEWITHSUNDEEP
syntaxisabelle
Wolfgang Jeltsch
Wolfgang Jeltsch

Reputation: 801

How can I define syntax for a binder with an additional argument in Isabelle?

I want to define a syntactic construct in Isabelle that has the form c ? x. p where c and p are values and x is a variable. This construct should translate to Input c (λx. p). It seems that this cannot be done via a binder annotation, since this construct has an additional argument c and furthermore cannot bind multiple variables. How can I define such a construct?

Upvotes: 2

Views: 89

Answers (1)

Wolfgang Jeltsch
Wolfgang Jeltsch

Reputation: 801

This is possible using the low-level syntax and translations facilities. Assuming that c is of a type channel, p and Input c (λx. p) are of a type process, and the desired precedence is 100, the construct can be defined as follows:

syntax
  "_Input" :: "channel ⇒ pttrn ⇒ process ⇒ process"
  ("(3_ ? _./ _)" [101, 0, 100] 100)
translations
  "c ? x. P" ⇌ "CONST Input c (λx. P)"

These kinds of syntax definitions are described in Subsection 8.2.1 of the Isabelle/Isar Reference Manual. To understand the above solution, it might be helpful to also look at Subsections 8.2.2 and 8.2.3, which partly explain how the more high-level infix, infixl, infixr, and binder constructs can be translated into low-level definitions. In addition, a look at the definitions of the set comprehension constructs in $ISABELLE_HOME/src/HOL/Set.thy could be useful.

Upvotes: 2

Related Questions