Gergely Buday (May 20 2024 at 15:48): Gergely Buday (May 20 2024 at 15:48):I would like to define a reverse syntax for lambda abstraction, namely:
exp | x would become \x. exp
I need to do a binder definition for this, but it is not clear how I could tell the system that I have this reverse syntax, first the body and then the bound variable.
Section 8.2.3 Binders in the Isar Reference Manual tells that the binder definition
definition c :: "(t1 => t2) => t3" (binder "sy" [p] q)
expands to "something like this":
definition c_binder :: "idts => t2 => t3" ("(3sy_./ _)" [0,p] q)
I guess this latter syntax allows me to define the reverse syntax but it is not clear how.
Can you give a hint on this?
Mathias Fleury (May 20 2024 at 15:55):is it possible to define an abbreviation over c that just swaps the order of the arguments and that has the binder definition?
Gergely Buday (May 20 2024 at 15:55):I will try, thanks
Gergely Buday (May 30 2024 at 13:10):@Mathias Fleury I see a problem that abbreviation handles values, but in a binder the first thing is a variable, not a value. In abbreviation, I need to give a type for the whole expression and it is not clear for me how could I tell Isabelle that the second argument is a variable.
Gergely Buday (May 31 2024 at 08:12):I got an answer on the mailing list that low-level syntax and translations should be used for this. The Isare Reference Manual at section 8.5.2 states that
Raw syntax and translations provides a slightly more low-level access to
the grammar and the form of resulting parse trees. It is often possible
to avoid this untyped macro mechanism, and use type-safe abbreviation
or notation instead. Some important situations where syntax and
translations are really need are as follows:
• Iterated replacement via recursive translations. For example, con-
sider list enumeration [a, b, c, d] as defined in theory HOL.List.
• Change of binding status of variables: anything beyond the built-in
binder mixfix annotation requires explicit syntax translations. For
example, consider the set comprehension syntax {x. P} as defined in
theory HOL.Set.
Last updated: Dec 21 2024 at 12:33 UTC